import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.Formula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;

public class GFTest {
    //[\forall (p5,\neg p1),
    // \exists (p5,p5),
    // \forall (p5,\neg p4),
    // \exists (p4,p4),
    // \forall (p4,p5),

    public void test1(){
        UnaryFormula p5=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p5"),false));
        UnaryFormula not_p1=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p1"),true));
        UnaryFormula not_p4=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p4"),true));
        UnaryFormula p4=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p4"),false));
        UnaryFormula not_r3=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r3"),true));
        UnaryFormula r1=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r1"),false));
        UnaryFormula r2=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r2"),false));

        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,p5,not_p1);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.EXIST,p5,p5);
        BinaryFormula bf3=new BinaryFormula(FormulaSign.ANY,p5,not_p4);
        BinaryFormula bf4=new BinaryFormula(FormulaSign.EXIST,p4,p4);
        BinaryFormula bf5=new BinaryFormula(FormulaSign.ANY,p4,p5);

        // \exists (\neg p1,\exists (\neg p1,\neg r3)),
        // \exists (p5,\exists (p4,r1)),
        // \forall (p5,\exists (\neg p4,\neg r3)),
        // \exists (\neg p1,\forall (\neg p1,r1)),
        // \exists (p5,\exists (p4,r2))]

        // \exists (\neg p1,\exists (\neg p1,\neg r3))
        BinaryFormula bf6=new BinaryFormula(FormulaSign.EXIST,not_p1,not_r3);
        BinaryFormula tf1=new BinaryFormula(FormulaSign.EXIST,not_p1,bf6);
        BinaryFormula bf7=new BinaryFormula(FormulaSign.EXIST,p4,r1);
        BinaryFormula tf2=new BinaryFormula(FormulaSign.EXIST,p5,bf7);
        BinaryFormula bf8=new BinaryFormula(FormulaSign.EXIST,not_p4,not_r3);
        BinaryFormula tf3=new BinaryFormula(FormulaSign.ANY,p5,bf8);
        BinaryFormula bf9=new BinaryFormula(FormulaSign.ANY,not_p1,r1);
        BinaryFormula tf4=new BinaryFormula(FormulaSign.EXIST,not_p1,bf9);
        BinaryFormula bf10=new BinaryFormula(FormulaSign.EXIST,p4,r2);
        BinaryFormula tf5=new BinaryFormula(FormulaSign.EXIST,p5,bf10);

        ArrayList<Formula> conditions=new ArrayList<>();
        conditions.add(bf1);
        conditions.add(bf2);
        conditions.add(bf3);
        conditions.add(bf4);
        conditions.add(bf5);
        conditions.add(tf1);
        conditions.add(tf2);
        conditions.add(tf3);
        conditions.add(tf4);
        conditions.add(tf5);

//        ArrayList<Proof> proofs=new ArrayList<>();
//        for (BinaryFormula bf:conditions) {
//            proofs.add(new ConclusionProof(bf));
//        }
//        for (Proof proof:proofs) {
//            System.out.println(proof);
//        }

        BinaryFormula c1=new BinaryFormula(FormulaSign.ANY,not_p4,r2);
        //BinaryFormula conclusion=new BinaryFormula()


        Proof result=Solve.solve(conditions,c1);
        System.out.println(result);



    }

    public static void main(String[] args) {
        GFTest test=new GFTest();
        test.test1();
    }
}
